Inductive type

타입 이론에서 어떤 타입이 재귀 타입이면서 동시에 합 타입이면 귀납 타입이라고 부른다.

Recursive sum types are called inductive datatypes, because mathematical induction may be used to prove statements about them. When programming, inductive datatypes are consumed through pattern matching and recursive functions. —Functional programming in Lean

프로그래밍 언어 예시

Lean에서는 이런 식으로 정의한다.

inductive Bool where
  | false : Bool
  | true : Bool

객체지향 언어에서는 클래스와 상속으로 표현할 수 있다. 다음은 자바 예시:

abstract class Bool {}

class True extends Bool {}
class False extends Bool {}

두 방식의 차이점:

However, the specifics of these representations are fairly different. In particular, each non-abstract class creates both a new type and new ways of allocating data. In the object-oriented example, True and False are both types that are more specific than Bool, while the Lean definition introduces only the new type Bool. —Functional programming in Lean

페아노 공리와 유사한 방식으로 자연수 정의하기:

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat